타입에 대한 내재적 관점과 외재적 관점
내재적(intrinsic) 관점과 외재적(extrinsic) 관점은 타입 이론에서 타입을 보는 두가지 관점이다.
내재적 관점은 "intrinsically typed", "처치 스타일(types à la Church)", "타입 검사 시스템(type checking system)", 외재적 관점은 "extrinsically typed", "커리 스타일(types à la Curry)", "타입 할당 시스템(type assignment system)" 등으로 불린다 [4, chap. DeBruijn, 3:8–9].
예시 : 단순 타입 λ-계산
단순 타입 λ-계산의 타입 시스템은 다음과 같이 두가지 방식으로 제시 될 수 있다.
내재적 타입 시스템
\[ \begin{array}{ll} A, B &::= A \to B \mid \ldots \\ M, N &::= \lambda x:A. M \mid M \ N \end{array} \] \[ \begin{prooftree} \AXC{$\Gamma , x:A \vdash M : B$} \UIC{$\Gamma \vdash \lambda x:A. M : A \to B$} \end{prooftree} \quad \begin{prooftree} \AXC{$\Gamma \vdash M : A \to B$} \AXC{$\Gamma \vdash N : A$} \BIC{$\Gamma \vdash M \ N : B$} \end{prooftree} \]
외재적 타입 시스템
\[ \begin{array}{ll} A, B &::= A \to B \mid \ldots \\ M, N &::= \lambda x. M \mid M \ N \end{array} \] \[ \begin{prooftree} \AXC{$\Gamma , x:A \vdash M : B$} \UIC{$\Gamma \vdash \lambda x. M : A \to B$} \end{prooftree} \quad \begin{prooftree} \AXC{$\Gamma \vdash M : A \to B$} \AXC{$\Gamma \vdash N : A$} \BIC{$\Gamma \vdash M \ N : B$} \end{prooftree} \]
타입 유일성
내재적 시스템에서는 타입의 유일성이 성립한다.
If \(\Gamma \vdash M : A\) and \(\Gamma \vdash M : B\), then \(A = B\)
외재적 시스템에서는 이러한 타입의 유일성이 성립하지 않는다.
증명보조기에서 내재적 타입 시스템의 구현
의존 타입이 있는 증명보조기에서 내재적인 타입 시스템을 형식화하는 경우, 항과 판단의 구분을 두지 않고 의존 타입을 이용해 형식화 하는 경우가 많다 [2, 4].
비교
[1, 2, 4] 등에서 내재적 타입 시스템과 외재적 타입 시스템을 비교하고 있다.
- 단순 타입 시스템의 경우, 의존 타입을 활용한 내재적 타입 시스템이 외재적 타입 시스템에 비해 더 적은 코드로 형식화 할 수 있다.
- β-축약은 타입과 무관하다. 내재적 타입 시스템에서는 이런 성질이 드러나지 않는다.
- 의존 타입 시스템을 내재적인 방식으로 형식화하기 까다로울 수 있다.